Nuprl Definition : rel_implies
11,40
postcript
pdf
rel_implies(
T
;
R1
;
R2
) ==
x
,
y
:
T
. (
x
R1
y
)
(
x
R2
y
)
latex
clarification:
rel_implies(
T
;
R1
;
R2
) ==
x
:
T
,
y
:
T
. (
x
R1
y
)
(
x
R2
y
)
latex
Definitions
x
:
A
.
B
(
x
)
,
P
Q
,
x
f
y
FDL editor aliases
rel_implies
origin
x,y:T. (x R1 y) 
(x R2 y)
x:T, y:T. (x R1 y) (x R2 y) x,y:T. (x R1 y) (x R2 y)
x:T, y:T. (x R1 y) (x R2 y) x:A. B(x) Q